| Definitions |  x:A. B(x), P   Q, P & Q, t  T,   x. t(x), S  T, suptype(S; T),  , Valtype(da;k), Top, f(x)?z, if b then t else f fi , tt, SQType(T), {T}, ff, rcv(l,tg),  b, lnk(k), tag(k), True, t.2, outl(x), t.1, sends k(v:T) on l:tagged(g,State(ds),v):dt, D realizes es. P(es), A c B, tag(e),  T, e@i. P(e), xL. P(x), f o g,  x:A. B(x), State(ds), State(ds), ES(the_w), E, P  Q, rcvs from e on l = L, P Q, E, state@i, sends-msgs(s;v;tg_f), (state when e), x(s), DeclaredType(ds;x),  , Unit, False, P  Q,  A, isrcv(e), lnk(e), SqStable(P),  , tagged-list-messages(s;v;L) |
| Lemmas | better-sends-rule, lsrc wf, fpf-join wf, Knd wf, fpf-single wf, lnk-decl wf, Kind-deq wf, Id wf, ma-state wf, ma-valtype wf, fpf-cap wf, rcv wf, decl-type wf, assert wf, isrcv wf, ldst wf, lnk wf, tagof wf, fpf wf, IdLnk wf, fpf-cap-single-join, fpf-join-cap-sq, top wf, fpf-trivial-subtype-top, fpf-dom wf, bool wf, eqtt to assert, fpf-single-dom, Knd sq, fpf-cap-single1, id-deq wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, lnk-decl-cap, Id sq, bool cases, bool sq, dsys wf, possible-world wf, fair-fifo wf, world wf, es-kind wf, es-lnk wf, w-es wf, es-isrcv wf, es-E wf, subtype rel wf, squash wf, true wf, es-valtype wf, subtype rel self, deq wf, isrcv-implies, IdLnk sq, es-loc wf, list-set-type2, es-tag wf, l member wf, map-map, member map, sq stable from decidable, decidable assert, l member set, list-set-type-property, decidable cand, decidable equal IdLnk, map wf, pi1 wf, tagged-list-messages-wf2, es-val wf, subtype rel list, decl-state wf, subtype rel product, subtype rel function, iff wf, es-sender wf, l before wf, es-locl wf, nat wf, w-isnull wf, w-a wf, pi2 wf, concat wf, sends-msgs wf, es-state-when wf, subtype rel dep function, es-vartype wf, l all wf2, l all map, es-rcv-kind, tagged-list-messages wf, fpf-ap wf, d-sub wf, d-single-sends wf |
Type, T:Type.
(State(ds)
lnk-decl(l;dt)